For the design of digital circuits (e.g., on the scale of Very Large Scale Integration (VLSI) technology), designers often employ computer-aided techniques. Standard languages such as Hardware Description Languages (HDLs) have been developed to describe digital circuits to aid in the design and simulation of complex digital circuits. Several hardware description languages, such as VHDL and Verilog, have evolved as industry standards. VHDL and Verilog are general-purpose hardware description languages that allow definition of a hardware model at the gate level, the register transfer level (RTL) or the behavioral level using abstract data types. As device technology continues to advance, various product design tools have been developed to adapt HDLs for use with newer devices and design styles.
In designing an integrated circuit with an HDL code, the code is first written and then compiled by an HDL compiler. The HDL source code describes at some level the circuit elements, and the compiler produces an RTL netlist from this compilation. The RTL netlist is typically a technology independent netlist in that it is independent of the technology/architecture of a specific vendor's integrated circuit, such as field programmable gate arrays (FPGA) or an application-specific integrated circuit (ASIC). The RTL netlist corresponds to a schematic representation of circuit elements (as opposed to a behavioral representation). A mapping operation is then performed to convert from the technology independent RTL netlist to a technology specific netlist, which can be used to create circuits in the vendor's technology/architecture. It is well known that FPGA vendors utilize different technology/architecture to implement logic circuits within their integrated circuits. Thus, the technology independent RTL netlist is mapped to create a netlist, which is specific to a particular vendor's technology/architecture.
After the synthesis transformation, equivalence checking can be performed to verify that the resulting design is equivalent to the original design. There are a number of techniques known in the art for equivalence checking, including functional approaches, automatic test pattern generation (ATPG) based approaches and incremental approaches. A functional approach uses Binary Decision Diagrams (BDD) to compare the circuit designs. When the Binary Decision Diagrams of two designs are isomorphic, the two designs are equivalent. An ATPG based approach proves the equivalence of two designs by proving that the stuck-at-0 is a redundant fault for their miter output. A variation of an ATPG based approach is the Boolean Satisfiability (SAT) technique. An incremental approach is based on reducing the miter circuit through the identification of internal equivalent pairs of the circuit nodes.
A hierarchical design approach breaks a large circuit into hierarchical blocks. Typically, each of the hierarchical blocks is individually synthesized for optimization and for design layout. Since the hierarchical boundaries isolate the hierarchical blocks from each other, the design of each of the hierarchical blocks can be individually verified. Since the hierarchical boundaries break a large problem into a series of smaller problems, the optimization and verification of the design can be efficiently performed at smaller scales. For a hierarchical design, synthesis transformation and optimization are typically limited within the hierarchical blocks. When no optimization is performed across the hierarchical boundaries, the verification can be performed based on the equivalence of the individual hierarchical blocks. When each of the hierarchical blocks is equivalent, the synthesized circuit design is equivalent to the original circuit design.
Alternatively, a hierarchical design can be flattened so that the entire circuit is optimized and verified as one unit. However, the computation resources typically limit the size of the entire circuit that can be optimized and verified as one flattened unit.
In certain situations, a designer may observe opportunities for optimization across the hierarchical boundary and manually optimize the design across the hierarchical boundary. To use a hierarchical approach in verifying the equivalence, the designer then manually prescribes user assertions for the equivalence checking programs to prevent the false result of non-equivalence when the equivalence of the hierarchical blocks is checked individually.